/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#10=GRFX35/FONT#11=GRK30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ ∧{Stanford Artificial Intelligence Project

␈↓ α∧␈↓Memo 1␈↓ 
:March 22, 1963

␈↓ α∧␈↓α␈↓ β⊃PREDICATE CALCULUS WITH "UNDEFINED" AS A TRUTH VALUE

␈↓ α∧␈↓␈↓ ελby John McCarthy

␈↓ α∧␈↓␈↓ αTWe␈α⊂would␈α∂like␈α⊂to␈α⊂use␈α∂predicate␈α⊂calculus␈α∂in␈α⊂the␈α⊂mathematical␈α∂theory␈α⊂of␈α⊂computation.␈α∂ In
␈↓ α∧␈↓particular,␈αwe␈αwould␈αlike␈α
to␈αwrite␈αformulas␈αinvolving␈α
recursively␈αdefined␈αpredicates␈αand␈α
functions.
␈↓ α∧␈↓The␈αtrouble␈αis␈αthat␈αrecursively␈αdefined␈αpredicates␈αare␈αnot␈αguaranteed␈αto␈αbe␈αdefined␈αfor␈αall␈αvalues
␈↓ α∧␈↓of their arguments, and therefore, it is not clear how to interpret formulas involving them.

␈↓ α∧␈↓␈↓ αTWe␈α
shall␈α
give␈α
an␈α
interpretation␈αof␈α
predicate␈α
calculus␈α
formulas␈α
involving␈α
partial␈αpredicates
␈↓ α∧␈↓and␈αextend␈αthe␈αnotions␈αof␈αtruth,␈αvalid␈αformula␈αand␈αtautology.␈α We␈αhave␈αthree␈αtruth␈αvalues,␈α
␈↓↓t␈↓␈αfor
␈↓ α∧␈↓␈↓↓true,␈↓␈α
␈↓↓f␈↓␈α
for␈α
␈↓↓false,␈↓␈α
and␈α␈↓↓u␈↓␈α
for␈α
␈↓↓undefined.␈↓␈α
The␈α
well-formed␈αformulas␈α
are␈α
the␈α
same␈α
as␈α
in␈αpredicate
␈↓ α∧␈↓calculus except that we have a new propositional operator * defined by

␈↓ α∧␈↓␈↓ β∧*␈↓↓t = t
␈↓ α∧␈↓↓␈↓ β∧*f = t
␈↓ α∧␈↓↓␈↓ β∧*u = f

␈↓ α∧␈↓We shall call our system EFC.

␈↓ α∧␈↓The truth of a formula is determined from its constituents as follows:

␈↓ α∧␈↓1. An elementary form ␈↓↓p(x,...,z)␈↓ is ␈↓↓true,␈↓ ␈↓↓false,␈↓ or ␈↓↓undefined␈↓ for each set of values of ␈↓↓x,...,z.␈↓

␈↓ α∧␈↓2. The truth values of propositional combinations is determined by the truth-tables.

␈↓"␈↓ α∧␈↓
␈↓ β$␈↓↓π␈↓
␈↓ βT~␈↓ βt␈↓↓¬π␈↓
␈↓ ∧4~␈↓ ∧T␈↓↓*π␈↓

␈↓"␈↓ α∧␈↓
␈↓ β∀αααα␈↓ βTβααααα␈↓ ∧4βααααα␈↓ ¬∀
␈↓"␈↓ α∧␈↓
␈↓ β$t␈↓ βT~␈↓ ∧∧f␈↓ ∧4~␈↓ ∧dt
␈↓"␈↓ α∧␈↓
␈↓ β$f␈↓ βT~␈↓ ∧∧t␈↓ ∧4~␈↓ ∧dt
␈↓"␈↓ α∧␈↓
␈↓ β$u␈↓ βT~␈↓ ∧∧u␈↓ ∧4~␈↓ ∧df


␈↓"␈↓ α∧␈↓
␈↓ β∀␈↓↓π␈↓r␈↓↓␈↓
␈↓ βT~␈↓ βt␈↓↓π∧␈↓r␈↓↓␈↓
␈↓ ∧4~␈↓ ∧T␈↓↓π∨␈↓r␈↓↓␈↓
␈↓ ¬∀~␈↓ ¬4␈↓↓π⊃␈↓r␈↓↓␈↓
␈↓ ¬t~␈↓ ε∀␈↓↓π≡␈↓r␈↓↓␈↓

␈↓"␈↓ α∧␈↓
␈↓ β∀αααα␈↓ βTβααααα␈↓ ∧4βααααα␈↓ ¬∀βααααα␈↓ ¬tβααααα␈↓ εT
␈↓"␈↓ α∧␈↓
␈↓ β∀tt␈↓ βT~␈↓ ∧∧t␈↓ ∧4~␈↓ ∧dt␈↓ ¬∀~␈↓ ¬Dt␈↓ ¬t~␈↓ ε$t
␈↓"␈↓ α∧␈↓
␈↓ β∀tf␈↓ βT~␈↓ ∧∧f␈↓ ∧4~␈↓ ∧dt␈↓ ¬∀~␈↓ ¬Df␈↓ ¬t~␈↓ ε$f
␈↓"␈↓ α∧␈↓
␈↓ β∀tu␈↓ βT~␈↓ ∧∧u␈↓ ∧4~␈↓ ∧dt␈↓ ¬∀~␈↓ ¬Du␈↓ ¬t~␈↓ ε$u
␈↓"␈↓ α∧␈↓
␈↓ β∀ft␈↓ βT~␈↓ ∧∧f␈↓ ∧4~␈↓ ∧dt␈↓ ¬∀~␈↓ ¬Dt␈↓ ¬t~␈↓ ε$f
␈↓"␈↓ α∧␈↓
␈↓ β∀ff␈↓ βT~␈↓ ∧∧f␈↓ ∧4~␈↓ ∧df␈↓ ¬∀~␈↓ ¬Dt␈↓ ¬t~␈↓ ε$t
␈↓"␈↓ α∧␈↓
␈↓ β∀fu␈↓ βT~␈↓ ∧∧f␈↓ ∧4~␈↓ ∧du␈↓ ¬∀~␈↓ ¬Dt␈↓ ¬t~␈↓ ε$u
␈↓"␈↓ α∧␈↓
␈↓ β∀ut␈↓ βT~␈↓ ∧∧u␈↓ ∧4~␈↓ ∧du␈↓ ¬∀~␈↓ ¬Du␈↓ ¬t~␈↓ ε$u
␈↓"␈↓ α∧␈↓
␈↓ β∀uf␈↓ βT~␈↓ ∧∧u␈↓ ∧4~␈↓ ∧du␈↓ ¬∀~␈↓ ¬Du␈↓ ¬t~␈↓ ε$u
␈↓"␈↓ α∧␈↓
␈↓ β∀uu␈↓ βT~␈↓ ∧∧u␈↓ ∧4~␈↓ ∧du␈↓ ¬∀~␈↓ ¬Du␈↓ ¬t~␈↓ ε$u
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓The truth values of the last two are in accordance with the definitions

␈↓ α∧␈↓␈↓ β∧␈↓↓π ⊃ ␈↓r␈↓↓ = ¬π ∨ ␈↓r␈↓↓
␈↓ α∧␈↓↓␈↓ β∧π ≡ ␈↓r␈↓↓ = (π ⊃ ␈↓r␈↓↓) ∧ (␈↓r␈↓↓ ⊃ π)

␈↓ α∧␈↓where␈α
␈↓↓=␈↓␈α
is␈α
used␈α
in␈α
its␈α
ordinary␈α
sense␈α∞as␈α
a␈α
metamathematical␈α
symbol.␈α
 They␈α
are␈α
the␈α
same␈α∞as␈α
the
␈↓ α∧␈↓conditional␈α∂expression␈α∂definitions␈α∂of␈α∂[1].␈α∂ As␈α∞explained␈α∂in␈α∂that␈α∂paper␈α∂the␈α∂noncommutativity␈α∞of
␈↓ α∧␈↓␈↓↓π∧␈↓r␈↓↓␈α␈↓and␈α␈↓↓π∨␈↓r␈↓↓␈α␈↓arises␈αfrom␈αthe␈αconvention␈αthat␈α␈↓↓π␈↓␈αis␈αevaluated␈αfirst,␈αso␈αthat␈αif␈α␈↓↓π␈↓␈αis␈αfalse,␈α␈↓r␈↓␈αneed␈αnot
␈↓ α∧␈↓be evaluated to get ␈↓↓π∧␈↓r␈↓↓.␈↓

␈↓ α∧␈↓3.␈α∞␈↓↓∀x.␈α∞π(x)␈α∞␈↓is␈α
true␈α∞if␈α∞␈↓↓π(x)␈↓␈α∞is␈α
true␈α∞for␈α∞all␈α∞x,␈α
undefined␈α∞if␈α∞␈↓↓π(x)␈↓␈α∞is␈α
undefined␈α∞for␈α∞some␈α∞␈↓↓x␈↓␈α∞and␈α
false
␈↓ α∧␈↓otherwise.

␈↓ α∧␈↓4.␈α
␈↓↓∃x.␈α
π(x)␈α
␈↓is␈α
true␈α
if␈α
␈↓↓π(x)␈↓␈α
is␈α
true␈α
for␈α
some␈α
␈↓↓x␈↓␈α
and␈α
is␈α
defined␈α
for␈α
all␈α
␈↓↓x,␈↓␈α
undefined␈α
if␈α
␈↓↓π(x)␈↓␈αis␈α
undefined
␈↓ α∧␈↓for some ␈↓↓x,␈↓ and false otherwise.

␈↓ α∧␈↓␈↓ αTIf␈αwe␈αconsider␈αformulas␈α
with␈αno␈αquantifiers␈αwe␈α
get␈αan␈αextended␈αpropositional␈αcalculus␈α
EPC.
␈↓ α∧␈↓A␈αformula␈αis␈αcalled␈α
a␈αtautology␈αif␈αit␈α
is␈αtrue␈αfor␈αall␈α
values␈αof␈αits␈αarguments.␈α
 Ordinary␈αtautologies
␈↓ α∧␈↓are␈α∪not␈α∀tautologies␈α∪of␈α∪EPC␈α∀since␈α∪they␈α∪are␈α∀undefined␈α∪if␈α∪all␈α∀the␈α∪propositional␈α∀variables␈α∪are
␈↓ α∧␈↓undefined.␈α∞ However,␈α∞if␈α∞␈↓↓π␈↓␈α∞is␈α∞an␈α
ordinary␈α∞tautology,␈α∞then␈α∞*␈↓↓π␈α∞⊃␈α∞π␈α
␈↓is␈α∞a␈α∞tautology␈α∞of␈α∞EPC␈α∞so␈α
that
␈↓ α∧␈↓formulas like

␈↓ α∧␈↓␈↓ β∧*␈↓↓(p⊃(q⊃p)) ⊃ (p⊃(q⊃p))

␈↓ α∧␈↓are tautologies.  Whether a formula is a tautology can be determined by truth tables.

␈↓ α∧␈↓The␈α
equivalence␈α
of␈α
two␈αformulas␈α
␈↓↓π␈↓␈α
and␈α
␈↓r␈↓␈αis␈α
not␈α
expressed␈α
by␈α
␈↓↓π␈α≡␈α
␈↓r␈↓↓␈α
␈↓being␈α
a␈αtautology,␈α
e.g.␈α
␈↓↓␈↓r␈↓↓␈α
≡␈α␈↓r␈↓↓␈α
␈↓is
␈↓ α∧␈↓not a tautology.  Therefore, we define

␈↓ α∧␈↓␈↓ β∧␈↓↓π ~ ␈↓r␈↓↓ = (*π ≡ *␈↓r␈↓↓) ∧ [*π ⊃ (π ≡ ␈↓r␈↓↓)],

␈↓ α∧␈↓and␈α␈↓↓π␈α~␈α␈↓r␈↓↓␈α␈↓␈αdoes␈αexpress␈αthe␈αequivalence␈αof␈α␈↓↓π␈↓␈αand␈α␈↓r␈↓.␈α This␈αis␈αthe␈αstrong␈αequivalence␈αof␈α[1].␈α The
␈↓ α∧␈↓weak equivalence of that paper is written

␈↓ α∧␈↓␈↓ β∧␈↓↓π ~␈↓#vw␈↓# ␈↓r␈↓↓ = *π ∧ *␈↓r␈↓↓ ⊃ (π ≡ ␈↓r␈↓↓)

␈↓ α∧␈↓where ␈↓↓π␈↓ and ␈↓r␈↓ do not involve *.

␈↓ α∧␈↓The following formulas are all tautologies

␈↓ α∧␈↓␈↓ β∧␈↓↓*(p ∧ q) ~ *p ∧ (p ⊃ *q)
␈↓ α∧␈↓↓␈↓ β∧*(p ∨ q) ~ *p ∧ (¬p ⊃ *q)
␈↓ α∧␈↓↓␈↓ β∧*(p ≡ q) ~ *p ∧ *q
␈↓ α∧␈↓↓␈↓ β∧*¬p ~ *p
␈↓ α∧␈↓↓␈↓ β∧**p
␈↓ α∧␈↓↓␈↓ β∧*(p ~ q)

␈↓ α∧␈↓The␈α
valid␈α
formulas␈αof␈α
EFC␈α
in␈αa␈α
domain␈α
are␈α
those␈αwhich␈α
are␈α
true␈αfor␈α
all␈α
assignments␈α
of␈αpartial
␈↓ α∧␈↓␈↓ u3


␈↓ α∧␈↓predicates␈αto␈αthe␈αpredicate␈αletters.␈α Many␈αquestions␈αabout␈αproof␈αprocedures␈αfor␈αEFC␈αare␈αanswered
␈↓ α∧␈↓by␈α⊃a␈α⊃construction␈α∩which␈α⊃gives␈α⊃for␈α∩every␈α⊃formula␈α⊃␈↓↓π␈↓␈α⊃of␈α∩EFC␈α⊃a␈α⊃formula␈α∩␈↓↓π␈↓#v1␈↓#␈α⊃␈↓of␈α⊃FC␈α∩(the␈α⊃usual
␈↓ α∧␈↓predicate␈α
calculus)␈αsuch␈α
that␈α
␈↓↓π␈↓␈αis␈α
valid␈α
in␈αthe␈α
domain␈αif␈α
and␈α
only␈αif␈α
␈↓↓π␈↓#v1␈↓#␈α
␈↓is␈αvalid.␈α
 Actually,␈αwe␈α
shall
␈↓ α∧␈↓construct␈αthree␈αformulas␈α␈↓↓π␈↓#v1␈↓#,␈απ␈↓#v2␈↓#␈α␈↓αa␈↓↓nd␈απ␈↓#v3␈↓#␈α␈↓of␈αFC␈αwhich␈αare␈αtrue␈αwhen␈α␈↓↓π␈↓␈αis␈αtrue,␈αfalse,␈αor␈αundefined
␈↓ α∧␈↓respectively.  The construction is given by the following table.

␈↓"␈↓ α∧␈↓
␈↓ βd␈↓↓π␈↓
␈↓ ∧4~␈↓ ¬4␈↓↓π␈↓β1␈↓↓␈↓
␈↓ ε4~␈↓ π4␈↓↓π␈↓β2␈↓↓␈↓
␈↓ λ4~␈↓ 	∧␈↓↓π␈↓β3␈↓↓␈↓

␈↓"␈↓ α∧␈↓
␈↓ β∀αααααααααα␈↓ ∧4βααααααααααααααα␈↓ ε4βααααααααααααααα␈↓ λ4ααααααααααααα␈↓ 
∧
␈↓"␈↓ α∧␈↓
␈↓ β∀␈↓↓p(x,...,z)␈↓
␈↓ ∧4~␈↓ ∧T␈↓↓p␈↓β1␈↓↓(x,...,z)␈↓
␈↓ ε4~␈↓ εT␈↓↓p␈↓β2␈↓↓(x,...,z)␈↓
␈↓ λ4~␈↓ λT␈↓↓p␈↓β3␈↓↓(x,...,z)
␈↓"␈↓ α∧␈↓↓␈↓ β∀¬π␈↓
␈↓ ∧4~␈↓ ∧T␈↓↓π␈↓β2␈↓↓␈↓
␈↓ ε4~␈↓ εT␈↓↓π␈↓β1␈↓↓␈↓
␈↓ λ4~␈↓ λT␈↓↓π␈↓β3␈↓↓
␈↓"␈↓ α∧␈↓↓␈↓ β∀*π␈↓
␈↓ ∧4~␈↓ ∧T␈↓↓π␈↓β1␈↓↓∨π␈↓β2␈↓↓␈↓
␈↓ ε4~␈↓ εT␈↓↓π␈↓β3␈↓↓␈↓
␈↓ λ4~␈↓ λT␈↓↓f
␈↓"␈↓ α∧␈↓↓␈↓ β∀π∧␈↓r␈↓↓␈↓
␈↓ ∧4~␈↓ ∧T␈↓↓π␈↓β1␈↓↓∧␈↓r␈↓↓␈↓β1␈↓↓␈↓
␈↓ ε4~␈↓ εT␈↓↓π␈↓β2␈↓↓∨(π␈↓β1␈↓↓␈↓r␈↓↓␈↓β2␈↓↓)␈↓
␈↓ λ4~␈↓ λT␈↓↓π␈↓β3␈↓↓∨(π␈↓β1␈↓↓∧␈↓r␈↓↓␈↓β3␈↓↓)
␈↓"␈↓ α∧␈↓↓␈↓ β∀π∨␈↓r␈↓↓␈↓
␈↓ ∧4~␈↓ ∧T␈↓↓π␈↓β1␈↓↓∨(π␈↓β2␈↓↓∧␈↓r␈↓↓␈↓β1␈↓↓)␈↓
␈↓ ε4~␈↓ εT␈↓↓π␈↓β2␈↓↓∧␈↓r␈↓↓␈↓β2␈↓↓␈↓
␈↓ λ4~␈↓ λT␈↓↓π␈↓β3␈↓↓∨(π␈↓β2␈↓↓∧␈↓r␈↓↓␈↓β3␈↓↓)
␈↓"␈↓ α∧␈↓↓␈↓ β∀π⊃␈↓r␈↓↓␈↓
␈↓ ∧4~␈↓ ∧T␈↓↓π␈↓β2␈↓↓∨(π␈↓β1␈↓↓∧␈↓r␈↓↓␈↓β1␈↓↓)␈↓
␈↓ ε4~␈↓ εT␈↓↓π␈↓β1␈↓↓∧␈↓r␈↓↓␈↓β2␈↓↓␈↓
␈↓ λ4~␈↓ λT␈↓↓π␈↓β3␈↓↓∨(π␈↓β1␈↓↓∧␈↓r␈↓↓␈↓β3␈↓↓)
␈↓"␈↓ α∧␈↓↓␈↓ β∀π≡␈↓r␈↓↓␈↓
␈↓ ∧4~␈↓ ∧T␈↓↓(π␈↓β1␈↓↓∧␈↓r␈↓↓␈↓β1␈↓↓)∨(π␈↓β2␈↓↓∧␈↓r␈↓↓␈↓β2␈↓↓))␈↓
␈↓ ε4~␈↓ εT␈↓↓(π␈↓β1␈↓↓∧␈↓r␈↓↓␈↓β2␈↓↓)∨(π␈↓β2␈↓↓∧␈↓r␈↓↓␈↓β1␈↓↓)␈↓
␈↓ λ4~␈↓ λT␈↓↓π␈↓β3␈↓↓∨␈↓r␈↓↓␈↓β3␈↓↓
␈↓"␈↓ α∧␈↓↓␈↓ β∀∀x.π␈↓
␈↓ ∧4~␈↓ ∧T␈↓↓∀x.π␈↓β1␈↓↓␈↓
␈↓ ε4~␈↓ εT␈↓↓(∃x.π␈↓β2␈↓↓)∧(∀x.¬π␈↓β3␈↓↓)␈↓
␈↓ λ4~␈↓ λT␈↓↓∃x.π␈↓β3␈↓↓
␈↓"␈↓ α∧␈↓↓␈↓ β∀∃x.π␈↓
␈↓ ∧4~␈↓ ∧T␈↓↓(∃x.π␈↓β1␈↓↓)∧(∀x.¬π␈↓β3␈↓↓)␈↓
␈↓ ε4~␈↓ εT␈↓↓(∀x.π␈↓β2␈↓↓)␈↓
␈↓ λ4~␈↓ λT␈↓↓∃x.π␈↓β3␈↓↓

␈↓ α∧␈↓That␈α
␈↓↓π␈↓#v1␈↓#,␈α
π␈↓#v2␈↓#␈α␈↓and␈α
␈↓↓π␈↓#v3␈↓#␈α
␈↓have␈αthe␈α
required␈α
properties␈αis␈α
obvious␈α
from␈αthe␈α
construction.␈α
 This␈αresult
␈↓ α∧␈↓shows␈αthat␈αEFC␈αis␈αsemi-decidable␈αso␈αthat␈αit␈αshould␈αbe␈αpossible␈αto␈αobtain␈αa␈αcomplete␈αset␈αof␈αaxioms
␈↓ α∧␈↓and␈αrules␈αof␈αinference.␈α The␈αmethod␈αof␈αsemantic␈αtableaux␈αcan␈αbe␈αapplied␈αdirectly␈αto␈αEFC,␈αbut,␈αat
␈↓ α∧␈↓least␈α⊂in␈α⊂its␈α∂most␈α⊂obvious␈α⊂form,␈α∂it␈α⊂is␈α⊂impractical␈α∂for␈α⊂all␈α⊂but␈α∂the␈α⊂simplest␈α⊂examples␈α⊂because␈α∂the
␈↓ α∧␈↓number of cases that has to be considered increases rapidly.

␈↓ α∧␈↓The␈α⊂choice␈α⊃of␈α⊂definitions␈α⊂for␈α⊃the␈α⊂quantifiers␈α⊃requires␈α⊂some␈α⊂explanation.␈α⊃ Our␈α⊂choice␈α⊃has␈α⊂the
␈↓ α∧␈↓disadvantage␈α
that␈α
one␈αcannot␈α
prove␈α
␈↓↓∃x.π(x)␈α␈↓simply␈α
by␈α
exhibiting␈αan␈α
a␈α
such␈αthat␈α
␈↓↓π(a)␈α
␈↓since␈αif␈α
some
␈↓ α∧␈↓␈↓↓π(b)␈α∂␈↓is␈α∂undefined␈α∂␈↓↓∃x.π(x)␈α∞␈↓is␈α∂considered␈α∂undefined.␈α∂ However,␈α∞the␈α∂other␈α∂possible␈α∂quantifiers␈α∞are
␈↓ α∧␈↓definable in terms of ours.  For example, we can define

␈↓ α∧␈↓␈↓ β∧␈↓↓(∃'x).π(x) = ∃x.*π(x)∧π(x)

␈↓ α∧␈↓which has the above mentioned property.

␈↓ α∧␈↓Note␈α∂of␈α∞February␈α∂8,␈α∂1979.␈α∞ This␈α∂AI␈α∂Memo␈α∞1␈α∂of␈α∂March␈α∞22,␈α∂1963␈α∂is␈α∞reprinted␈α∂with␈α∂only␈α∞trivial
␈↓ α∧␈↓notational␈α∞changes.␈α∞ The␈α∞reference,␈α∞which␈α∞was␈α∞omitted␈α∞from␈α∞the␈α∞original,␈α∞is␈α∞to␈α∞␈↓αMcCarthy,␈α
John␈↓
␈↓ α∧␈↓(1963)␈α
"A␈α
Basis␈α
for␈α
a␈α
Mathematical␈α
Theory␈α
of␈α
Computation",␈α
in␈α
P.␈α
Braffort␈α
and␈α
D.␈α
Hirschberg
␈↓ α∧␈↓(eds.),␈α⊗␈↓↓Computer␈α⊗Programming␈α⊗and␈α⊗Formal␈α⊗Systems␈↓,␈α⊗pp.␈α⊗33-70.␈α↔ North-Holland␈α⊗Publishing
␈↓ α∧␈↓Company, Amsterdam.